Nuprl Lemma : det_ideal_defines_eqv 13,42

r:CRng, a:Ideal(r){i}, d:detach_fun(|r|;a). EquivRel(|r|;u,v.(d(u +r (-r(v))))) 
latex


Uprings 1
Definitions of StatementRng, CRng, Ideal(r){i}
Definitionst  T, x:AB(x), P & Q, x,yt(x;y), , P  Q, x f y, P  Q, True, T, False, Rng, Ideal(r){i}, CRng, {T}, detach_fun(T;A), x(s1,s2), P  Q, A, P  Q, Dec(P), XM
Lemmascrng wf, ideal wf, rng car wf, detach fun wf, detach fun properties, squash wf, rng minus wf, rng plus wf, assert wf, equiv rel functionality wrt iff, squash thru equiv rel, ideal defines eqv, ideal p wf

origin